the_es:event_system{i:l}, e,e',y:es-E(the_es).
l_before(e'; y; before(e); es-E(the_es))  es-locl(the_es; e'; y) 

latex

Definitions

x:A. B(x), P  Q, before(e), t  T, prop{i:l}, x. t(x), Y, if b then t else f fi , tt, ff, P  Q, P  Q, P  Q, A, x:A. B(x), ||as||, T, True, subtype(S; T), suptype(S; T), A  B, ge(i; j), t  ...$L, False, (x  l), , A c B, P  Q, wellfounded{i:l}(A; x,y.R(x;y)), x(s), guard(T), , Unit, decidable(P), l_before(x; y; l; T), sublist(T; L1; L2), int_seg(i; j), increasing(f; k), l[i], hd(l), nth_tl(n;as), i z j, b, i <z j, lelt(i; j; k),

Lemmas

es-locl-wellfnd, es-E wf, l before wf, es-before wf, es-locl wf, es-first wf, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, event system wf, all functionality wrt iff, false wf, implies functionality wrt iff, nil before, decidable es-E-equal, es-pred wf, append wf, member-es-before, int seg wf, squash wf, true wf, length append, increasing wf, length wf1, select wf, length nil, length cons, non neg length, select append front, le wf, es-pred-locl, not functionality wrt iff, l member wf, cons member, or functionality wrt iff, nil member, l before append front